Introduction in [Giesl & Middeldorp - RTA'99]

Summary: ExIntrod_GM99

• CS-TRS format
• OBJ format
• Negative results:
  1. CSRPO
  2. Lucas' transformation (Extra variables)
• Positive results:

CS-TRS ExIntrod_GM99 (file ExIntrod_GM99.csr)

Functions:  primes sieve from s 0 cons head tail if true false filter divides

Constructors:  s 0 cons true false divides

Variables:  X Y Z

Arities: 

ar(primes) = 0
ar(sieve) = 1
ar(from) = 1
ar(s) = 1
ar(0) = 0
ar(cons) = 2
ar(head) = 1
ar(tail) = 1
ar(if) = 3
ar(true) = 0
ar(false) = 0
ar(filter) = 2
ar(divides) = 2

Replacement map: 

µ(primes)={}
µ(sieve)={1}
µ(from)={1}
µ(s)={1}
µ(0)={}
µ(cons)={1}
µ(head)={1}
µ(tail)={1}
µ(if)={1}
µ(true)={}
µ(false)={}
µ(filter)={1,2}
µ(divides)={1,2}

Rules:  (file ExIntrod_GM99)   

primes -> sieve(from(s(s(0))))
from(X) -> cons(X,from(s(X)))
head(cons(X,Y)) -> X
tail(cons(X,Y)) -> Y
if(true,X,Y) -> X
if(false,X,Y) -> Y
filter(s(s(X)),cons(Y,Z)) -> if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))
sieve(cons(X,Y)) -> cons(X,filter(X,sieve(Y)))

The CS-TRS in OBJ format (file ExIntrod_GM99.obj):

obj ExIntrod_GM99 is
  sort S .
  op primes : -> S .
  op sieve : S -> S .
  op from : S -> S .
  op s : S -> S .
  op 0 : -> S .
  op cons : S S -> S [strat (1 0)] .
  op head : S -> S .
  op tail : S -> S .
  op if : S S S -> S [strat (1 0)] .
  op true : -> S .
  op false : -> S .
  op filter : S S -> S .
  op divides : S S -> S .
  vars X Y Z : S .
  eq primes = sieve(from(s(s(0)))) .
  eq from(X) = cons(X,from(s(X))) .
  eq head(cons(X,Y)) = X .
  eq tail(cons(X,Y)) = Y .
  eq if(true,X,Y) = X .
  eq if(false,X,Y) = Y .
  eq filter(s(s(X)),cons(Y,Z)) = if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))) .
  eq sieve(cons(X,Y)) = cons(X,filter(X,sieve(Y))) .
endo

Negative results

1. The µ-termination of ExIntrod_GM99 cannot be proved by using CSRPO (counterexample due to Albert Rubio):

      Possible ingredients:
   
      m(cons,2)=from
      m(if,2)=filter   ===>   since  otherwise the filter rule cannot be proved.
   
      primes> sieve,from,s,0
      from> cons, from',s
   
      add>s
      first > nil
      first > cons
      first> from
      tail > from
      filter > if,divides
   
   
      marked versions:
    
      primes > sieve(from(s(s(0))))
   
      from(X) > cons(X,from'(s(X)))
   
      tail(cons(X,Y_{from})) > Y
   
      if(true,X_{filter},Y) > X  !  ==> if > filter
      if(false,X,Y) > Y
   
      filter(s(s(X)),cons(Y,Z_{from})) > if(divides(s(s(X)),Y),filter'(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))
      ????? Fails since filter > if is needed
   
      sieve(cons(X,Y)) > cons(X,filter(X,sieve(Y)))
      

2. The µ-termination of ExIntrod_GM99 cannot be proved by using Lucas' transformation. The TRS ExIntrod_GM99_L:

       primes -> sieve(from(s(s(0))))
       from(X) -> cons(X)
       head(cons(X)) -> X
       tail(cons(X)) -> Y
       if(true) -> X
       if(false) -> Y
       filter(s(s(X)),cons(Y)) -> if(divides(s(s(X)),Y))
       sieve(cons(X)) -> cons(X)
       

   contains extra variables.

Positive results